-- | This module provides functions to resolve names in specs.
--
-- There are two major namespaces in LH:
--
-- 1) The names of Haskell entities
-- 2) The names of logic entities
--
-- At the moment LH resolves names to Haskell entities, while resolving logic
-- entities remains work in progress.
--
-- Haskell entities include all functions that LH might reflect, or types that
-- might be referred in refinement types, type aliases or other annotations.
--
-- Logic entities include the names of reflected functions, inlined functions,
-- uninterpreted functions, predefined functions, local bindings, reflected data
-- constructors and parameters of Haskell functions in specs of other local
-- bindings.
--
-- The resolution pipeline goes as follows.
--
-- * First the module specs are parsed into a 'BareSpecParsed'.
--   Here all names are unresolved.
-- * Next the names of Haskell entities are resolved by 'resolveLHNames'.
--   For now, this pass doesn't change the type of the names.
-- * Next the names of logic entities are resolved. This pass produces
--   a 'BareSpecLHName', where 'Symbol's are replaced with 'LHName'.
--
-- 'BareSpecLHName' has an approximate bijection to 'BareSpec' via a 'LogicNameEnv'
-- which allows to convert 'LHName' to an unambiguous form of 'Symbol'
-- and back. The bijection is implemented with the functions 'toBareSpecLHName'
-- and 'fromBareSpecLHName'. This allows to use liquid-fixpoint functions
-- unmodified as they will continue to operate on (now unambiguous) Symbols.
-- The bijection is approximate because in the roundtrip the representation of
-- LHName's might change.
--
-- At the same time, the 'BareSpecLHName' form is kept to serialize and to
-- resolve names of modules that import the specs.
--

{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE TypeApplications           #-}

module Language.Haskell.Liquid.LHNameResolution
  ( resolveLHNames
  , resolveSymbolToTcName
  , exprArg
  , fromBareSpecLHName
  , toBareSpecLHName
  , symbolToLHName
  , LogicNameEnv(..)
  ) where

import qualified Liquid.GHC.API         as GHC hiding (Expr, panic)
import qualified Language.Haskell.Liquid.GHC.Interface   as LH
import qualified Language.Haskell.Liquid.GHC.Misc        as LH
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp

import           Control.Monad.Except (ExceptT, runExceptT, throwError)
import           Control.Monad ((<=<), mplus, unless, void)
import           Control.Monad.Identity
import           Control.Monad.State.Strict
import           Data.Bifunctor (first, second)
import qualified Data.Char                               as Char
import           Data.Coerce (coerce)
import           Data.Data (Data, gmapM)
import           Data.Generics (extM)


import qualified Data.HashSet                            as HS
import qualified Data.HashMap.Strict                     as HM
import           Data.List (find, isSuffixOf, nubBy, partition)
import           Data.List.Extra (dropEnd)
import qualified Data.Map as Map
import           Data.Maybe (fromMaybe, listToMaybe, mapMaybe, maybeToList)
import qualified Data.Text                               as Text
import qualified GHC.Types.Name.Occurrence

import           Language.Fixpoint.Types as F hiding (Error, panic)
import qualified Language.Haskell.Liquid.Bare.Resolve as Resolve
import           Language.Haskell.Liquid.Bare.Types (LocalVars(lvNames), LocalVarDetails(lvdLclEnv))
import           Language.Fixpoint.Misc as Misc
import           Language.Haskell.Liquid.Name.LogicNameEnv
import qualified Language.Haskell.Liquid.Types.DataDecl as DataDecl
import           Language.Haskell.Liquid.Types.Errors (TError(ErrDupNames, ErrResolve), panic)
import           Language.Haskell.Liquid.Types.Specs as Specs
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.UX.Config
import           Language.Haskell.Liquid.WiredIn

import qualified Text.PrettyPrint.HughesPJ as PJ
import qualified Text.Printf               as Printf

-- | Collects type aliases from the current module and its dependencies.
--
-- By construction, type alises from transitive dependencies are neglected (see 'moduleAliases').
-- We do so because all type aliases in scope are added to the 'LiftedSpec' later.
-- Aliases with the same unqualified name coexist during name resolution,
-- as long as we have a means to disambiguate (namely, by qualifing the import).
-- In this case, when building the 'LiftedSpec' we carry only the first such alias according
-- to lexicographic order.
collectTypeAliases
  :: GHC.ImportedMods
  -> GHC.Module
  -> BareSpecParsed
  -> TargetDependencies
  -> InScopeEnv (RTAlias Symbol ())
collectTypeAliases impMods thisModule spec deps =
    let bsAliases = mkAliasEnv thisModule impMods (thisModule, bsNames)
        bsNames = [ (val . rtName $ rta, void rta) | rta <- aliases spec]
        depAliases = map (mkAliasEnv thisModule impMods) $
          [ (m, depNames)
          | (sm, lspec) <- HM.toList (getDependencies deps)
          , let m = GHC.unStableModule sm
          , let depNames = [ (val . rtName $ rta , void rta)
                           | rta <- HS.toList $ liftedAliases lspec
                           ]
          ]
     in
        unionAliasEnvs $ bsAliases : depAliases

--------------------------------------------------------------------------------
-- | [NOTE:EXPRESSION-ALIASES]:
--
-- In a lifted spec, expression aliases include fully unfolded predicate,
-- inline, and define annotations. By contrast, a bare spec’s expression
-- aliases include only predicate aliases. This is because symbols from these
-- three kinds of annotations are unfolded uniformly in logical expressions
-- during spec lifting.
--
-- Inlines and defines are converted to expression aliases via 'lmapEalias',
-- which assigns them a 'GeneratedLogicName'. This allows us to distinguish
-- them from predicate aliases, which should be the only 'LogicName's among
-- expression aliases.
--
-- Here, we collect the symbols of inlines and defines from expression aliases
-- to identify their uses when resolving logic variable names.
-- This should be redundant when these aliases are resolved via the
-- logic environments and a dedicated lifted field for inlines is added.
--------------------------------------------------------------------------------
collectInlinesAndDefines:: TargetDependencies -> HS.HashSet Symbol
collectInlinesAndDefines deps = HS.unions
  [ HS.map lhNameToResolvedSymbol depInlinesAndDefines
  | (_, lspec) <- HM.toList (getDependencies deps)
  , let exprAliases = HS.map (val . rtName) $ liftedEaliases lspec
        depInlinesAndDefines = HS.filter (not . isResolvedLogicName) exprAliases
   ]

-- | Converts occurrences of LHNUnresolved to LHNResolved using the provided
-- type aliases and GlobalRdrEnv.
resolveLHNames
  :: Config
  -> GHC.Module
  -> LocalVars
  -> GHC.ImportedMods
  -> GHC.GlobalRdrEnv
  -> BareSpecParsed
  -> TargetDependencies
  -> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependencies =
  flip evalState RenameOutput { roErrors = [], roUsedNames = [], roUsedDataCons = mempty } $
    runExceptT $ do
      -- Prepare type aliases for resolution.
      sp0 <- lift $ fixExpressionArgsOfTypeAliases taliases $ resolveBoundVarsInTypeAliases bareSpec0

      checkErrors

      -- First resolution pass: A generic traversal that resolves names
      -- of Haskell entities and type alias binders.
      sp1 <- lift $ mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) sp0

      -- Data decls contain fieldnames that introduce measures with the
      -- same names. We resolve them before constructing the logic
      -- environments.
      dataDecls <- lift $ mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1)
      let sp2 = sp1 {dataDecls}

      checkErrors

      -- Second resolution pass: a traversal to resolve logic names using the following
      -- lookup environments.
      let (inScopeEnv, logicNameEnv0, privateReflectNames) =
            makeLogicEnvs impMods thisModule sp2 dependencies

          -- Add resolved local defines to the logic map.
          lmap1 = lmap <> mkLogicMap (HM.fromList $
                   [ (F.val $ lhNameToResolvedSymbol <$> k,
                      (val <$> v) { lmVar = lhNameToResolvedSymbol <$> k })
                   | (k,v) <- defines sp2 ])
      sp3 <- lift $ fromBareSpecLHName <$>
                  resolveLogicNames
                    cfg
                    thisModule
                    inScopeEnv
                    globalRdrEnv
                    lmap1
                    localVars
                    logicNameEnv0
                    privateReflectNames
                    depsInlinesAndDefines
                    sp2

      checkErrors

      dcs <- gets roUsedDataCons
      return (sp3 { usedDataCons = dcs }, logicNameEnv0, lmap1)
  where
    -- Early exit name resolution if errors are found and pass them to the output.
    checkErrors :: ExceptT [Error] (StateT RenameOutput Identity) ()
    checkErrors = do
      es <- gets roErrors
      unless (null es) (throwError es)

    -- We collect type aliases before resolving names so we have a means to disambiguate
    -- imported and local ones (according to their resolution status).
    taliases = collectTypeAliases impMods thisModule bareSpec0 dependencies
    depsInlinesAndDefines = collectInlinesAndDefines dependencies

    -- Add defines from dependencies to the logical map.
    lmap =
        (LH.listLMap <>) $
        mconcat $
        map (mkLogicMap . HM.map (fmap lhNameToResolvedSymbol) . liftedDefines) $
        HM.elems $
        getDependencies dependencies

    resolveFieldLogicName n =
      case n of
        LHNUnresolved LHLogicNameBinder s -> pure $ makeLogicLHName s thisModule Nothing
        _ -> panic Nothing $ "unexpected name: " ++ show n

    resolveLHName lname =
      case val lname of
        LHNUnresolved (LHTcName lcl) s
          | isTuple s ->
            pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s
          | isList s ->
            pure $ LHNResolved (LHRGHC GHC.listTyConName) s
          | s == "*" ->
            pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s
          | otherwise ->
            case resolveTypeAlias taliases s of
              -- Priority is given to aliases defined in the current module,
              -- so name occurrences are resolved using them, disregarding
              -- any imported aliases with the same name.
              -- This allows the user to shadow imported aliases.
              FoundTypeAliases { tarLocallyDefined = [(m, _, _)] } ->
                pure $ makeLogicLHName (LH.dropModuleNames s) m Nothing
              FoundTypeAliases { tarImported = [(_, lh, _)]
                               , tarLocallyDefined = []} | lcl == LHAnyModuleNameF ->
                pure lh
              -- If multiple matches are found, report the ambiguous name and return it.
              tar@(FoundTypeAliases { }) -> do addError $ errResolveTypeAlias (s <$ lname) tar
                                               pure $ val lname
              NoSuchTypeAlias alts -> lookupGRELHName alts (LHTcName lcl) lname s listToMaybe
        LHNUnresolved ns@(LHVarName lcl) s
          | isDataCon s ->
              lookupGRELHName [] (LHDataConName lcl) lname s listToMaybe
          | otherwise ->
              lookupGRELHName [] ns lname s
                (fmap (either id GHC.getName) . Resolve.lookupLocalVar localVars (atLoc lname s))
        LHNUnresolved LHLogicNameBinder s ->
          pure $ makeLogicLHName s thisModule Nothing
        n@(LHNUnresolved LHLogicName _) ->
          -- This one will be resolved by resolveLogicNames
          pure n
        LHNUnresolved ns@(LHDataConName _) s -> lookupGRELHName [] ns lname s listToMaybe
        n@LHNResolved { } -> pure n

    lookupGRELHName alts ns lname s localNameLookup =
      case maybeDropImported ns $ GHC.lookupGRE globalRdrEnv (mkLookupGRE ns s) of
        [e] -> do
          let n = GHC.greName e
              n' = fromMaybe n $ localNameLookup [n]
          pure $ LHNResolved (LHRGHC n') s
        es@(_:_) -> do
          let topLevelNames = map GHC.greName es
          case localNameLookup topLevelNames of
            Just n | notElem n topLevelNames ->
              pure $ LHNResolved (LHRGHC n) s
            _ -> do
              addError
                (ErrDupNames
                   (LH.fSrcSpan lname)
                   "variable"
                   (pprint s)
                   (map (PJ.text . GHC.showPprUnsafe) es)
                )
              pure $ val lname
        [] ->
          case localNameLookup [] of
            Just n' ->
              pure $ LHNResolved (LHRGHC n') s
            Nothing -> do
              addError
                (errResolve alts (nameSpaceKind ns) "Cannot resolve name" (s <$ lname))
              pure $ val lname

    maybeDropImported ns es
      | localNameSpace ns = filter GHC.isLocalGRE es
      | otherwise = es

    localNameSpace = \case
      LHDataConName lcl -> lcl == LHThisModuleNameF
      LHVarName lcl -> lcl == LHThisModuleNameF
      LHTcName lcl -> lcl == LHThisModuleNameF
      LHLogicNameBinder -> False
      LHLogicName -> False

    nameSpaceKind :: LHNameSpace -> PJ.Doc
    nameSpaceKind = \case
      LHTcName LHAnyModuleNameF -> "type constructor"
      LHTcName LHThisModuleNameF -> "locally-defined type constructor"
      LHDataConName LHAnyModuleNameF -> "data constructor"
      LHDataConName LHThisModuleNameF -> "locally-defined data constructor"
      LHVarName LHAnyModuleNameF -> "variable"
      LHVarName LHThisModuleNameF -> "variable from the current module"
      LHLogicNameBinder -> "logic name binder"
      LHLogicName -> "logic name"

    isDataCon s = case Text.uncons (Text.takeWhileEnd (/= '.') (symbolText s)) of
      Just (c, _) -> Char.isUpper c || c == ':'
      Nothing -> False

tupleArity :: Symbol -> Int
tupleArity s =
      let a = read $ drop 5 $ symbolString s
       in if a > 64 then
            error $ "tupleArity: Too large (more than 64): " ++ show a
          else
            a

errResolve :: [Symbol] -> PJ.Doc -> String -> LocSymbol -> Error
errResolve alts k msg ls =
  ErrResolve
    (LH.fSrcSpan ls)
    k
    (pprint $ val ls)
    (if null alts then
        PJ.text msg
      else
        PJ.text msg PJ.$$
        PJ.sep (PJ.text "Maybe you meant one of:" : map pprint alts)
    )


-- | Produces an LHName from a symbol by looking it in the rdr environment.
resolveSymbolToTcName :: GHC.GlobalRdrEnv -> LocSymbol -> Either Error (Located LHName)
resolveSymbolToTcName globalRdrEnv lx
    | isTuple s =
      pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s <$ lx
    | isList s =
      pure $ LHNResolved (LHRGHC GHC.listTyConName) s <$ lx
    | s == "*" =
      pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s <$ lx
    | otherwise =
      case GHC.lookupGRE globalRdrEnv (mkLookupGRE (LHTcName LHAnyModuleNameF) s) of
        [e] -> Right $ LHNResolved (LHRGHC $ GHC.greName e) s <$ lx
        [] -> Left $ errResolve [] "type constructor" "Cannot resolve name" lx
        es -> Left $ ErrDupNames
                (LH.fSrcSpan lx)
                "type constructor"
                (pprint s)
                (map (PJ.text . GHC.showPprUnsafe) es)
  where
    s = val lx

-- | Resolving logic names can produce errors and new names to add to the
-- environment. New names might be produced when encountering data constructors
-- or functions from the logic map.
data RenameOutput = RenameOutput
    { roErrors :: [Error]
      -- | Names of used data constructors, and names of used reflected
      -- functions and used logic map names
    , roUsedNames :: [LHName]
      -- | Names of used data constructors
    , roUsedDataCons :: HS.HashSet LHName
    }

addError :: Error -> State RenameOutput ()
addError e = modify (\ro -> ro { roErrors = e : roErrors ro })

addName :: LHName -> State RenameOutput ()
addName n = modify (\ro -> ro { roUsedNames = n : roUsedNames ro })

addDataConsName :: LHName -> State RenameOutput ()
addDataConsName n = modify (\ro -> ro { roUsedDataCons = HS.insert n (roUsedDataCons ro) })

mkLookupGRE :: LHNameSpace -> Symbol -> GHC.LookupGRE GHC.GREInfo
mkLookupGRE ns s =
    let m = LH.takeModuleNames s
        n = LH.dropModuleNames s
        nString = symbolString n
        oname = GHC.mkOccName (mkGHCNameSpace ns) nString
        rdrn =
          if m == "" then
            GHC.mkRdrUnqual oname
          else
            GHC.mkRdrQual (GHC.mkModuleName $ symbolString m) oname
     in GHC.LookupRdrName rdrn (mkWhichGREs ns)
  where
    mkWhichGREs :: LHNameSpace -> GHC.WhichGREs GHC.GREInfo
    mkWhichGREs = \case
      LHTcName _ -> GHC.SameNameSpace
      LHDataConName _ -> GHC.SameNameSpace
      LHVarName _ -> GHC.RelevantGREs
        { GHC.includeFieldSelectors = GHC.WantNormal
        , GHC.lookupVariablesForFields = True
        , GHC.lookupTyConsAsWell = False
        }
      LHLogicNameBinder -> panic Nothing "mkWhichGREs: unexpected namespace LHLogicNameBinder"
      LHLogicName -> panic Nothing "mkWhichGREs: unexpected namespace LHLogicName"

    mkGHCNameSpace = \case
      LHTcName _ -> GHC.tcName
      LHDataConName _ -> GHC.dataName
      LHVarName _ -> GHC.Types.Name.Occurrence.varName
      LHLogicNameBinder -> panic Nothing "mkGHCNameSpace: unexpected namespace LHLogicNameBinder"
      LHLogicName -> panic Nothing "mkGHCNameSpace: unexpected namespace LHLogicName"

-- | Changes unresolved names to local resolved names in the body of type
-- aliases.
resolveBoundVarsInTypeAliases :: BareSpecParsed -> BareSpecParsed
resolveBoundVarsInTypeAliases = updateAliases resolveBoundVars
  where
    resolveBoundVars boundVars = \case
      LHNUnresolved (LHTcName lcl) s ->
        if elem s boundVars then
          LHNResolved (LHRLocal s) s
        else
          LHNUnresolved (LHTcName lcl) s
      n ->
        error $ "resolveLHNames: Unexpected resolved name: " ++ show n

    -- Applies a function to the body of type aliases, passes to every call the
    -- arguments of the alias.
    updateAliases f spec =
       spec
            { aliases = [ a { rtBody = mapLHNames (f args) (rtBody a) }
                        | a <- aliases spec
                        , let args = rtTArgs a ++ rtVArgs a
                        ]
            }

-- | The expression arguments of type aliases are initially parsed as
-- types. This function converts them to expressions.
--
-- For instance, in @Prop (Ev (plus n n))@ where `Prop` is the alias
--
-- > {-@ type Prop E = {v:_ | prop v = E} @-}
--
-- the parser builds a type for @Ev (plus n n)@.
-- | @fixExpressionArgsOfTypeAliases taliases spec@ converts types to
-- values when they appear in value positions of type aliases according
-- to @taliases@.
--
-- The expression arguments of type aliases are initially parsed as
-- types. This function converts them to expressions.
--
-- For instance, in @Prop (Ev (plus n n))@ where `Prop` is the alias
--
-- > {-@ type Prop E = {v:_ | prop v = E} @-}
--
-- the parser builds a type for @Ev (plus n n)@, making a type
-- constructor of @Ev@ and type variables of @plus@ and @n@. But
-- @Ev@ is really a data constructor, @plus@ is a function, and @n@
-- is a value. 
fixExpressionArgsOfTypeAliases
  :: InScopeEnv (RTAlias Symbol ())
  -> BareSpecParsed
  -> StateT RenameOutput Identity BareSpecParsed
fixExpressionArgsOfTypeAliases taliases = mapMBareTypes go
  where
    go :: BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
    go (RApp c@(BTyCon { btc_tc = lname@(Loc _ _ (LHNUnresolved (LHTcName _) s)) }) ts rs r)
      | tar@(FoundTypeAliases imported local) <- resolveTypeAlias taliases s =
          case (imported, local) of
               -- Local alias definitions get priority over imported ones.
               -- This allows the user to shadow imported aliases.
               (_ ,[(_, _, rta)]) ->
                 RApp <$> pure c <*> fixExprArgs (btc_tc c) rta (mapM go ts) <*> mapM goRef rs <*> pure r
               ([(_, _, rta)] , []) ->
                 RApp <$> pure c <*> fixExprArgs (btc_tc c) rta (mapM go ts) <*> mapM goRef rs <*> pure r
               -- Report ambiguos name and continue traversing.
               _ -> do
                 addError $ errResolveTypeAlias (s <$ lname) tar
                 RApp <$> pure c <*> mapM go ts <*> mapM goRef rs <*> pure r
    go (RApp c ts rs r)    = RApp <$> pure c <*> mapM go ts <*> mapM goRef rs <*> pure r
    go (RAppTy t1 t2 r)    = RAppTy <$> go t1 <*> go t2 <*> pure r
    go (RFun  x i t1 t2 r) = RFun <$> pure x <*> pure i <*> go t1 <*> go t2 <*> pure r
    go (RAllT a t r)       = RAllT <$> pure a <*> go t <*> pure r
    go (RAllP a t)         = RAllP a <$> go t
    go (RAllE x t1 t2)     = RAllE x <$> go t1 <*> go t2
    go (REx x t1 t2)       = REx  x <$> go t1 <*> go t2
    go (RRTy e r o t)      = RRTy  e r o  <$> go t
    go t@RHole{}           = pure t
    go t@RVar{}            = pure t
    go t@RExprArg{}        = pure t
    goRef (RProp ss t)     = RProp ss <$> go t

    fixExprArgs lname rta mts = do
      ts <- mts
      let n = length (rtTArgs rta)
          (targs, eargs) = splitAt n ts
          msg = "FIX-EXPRESSION-ARG: " ++ showpp (rtName rta)
          toExprArg = exprArg (LH.fSourcePos lname) msg
      pure $ targs ++ [ RExprArg $ toExprArg e <$ lname | e <- eargs ]

mapMBareTypes :: forall m a.(Data a, Monad m) => (BareTypeParsed -> m BareTypeParsed) -> a -> m a
mapMBareTypes f  = go
  where
    go :: forall b. Data b => b -> m b
    go = gmapM (go `extM` f)

-- | exprArg converts a tyVar to an exprVar because parser cannot tell
--   this function allows us to treating (parsed) "types" as "value"
--   arguments, e.g. type Matrix a Row Col = List (List a Row) Col
--   Note that during parsing, we don't necessarily know whether a
--   string is a type or a value expression. E.g. in tests/pos/T1189.hs,
--   the string `Prop (Ev (plus n n))` where `Prop` is the alias:
--     {-@ type Prop E = {v:_ | prop v = E} @-}
--   the parser will chomp in `Ev (plus n n)` as a `BareType` and so
-- | @exprArg@ converts a type to a value.
--   
--   At parse time the arguments of type aliases are all treated as types.
--   This needs fixing before verification because some arguments are
--   meant to be values. Hence, this function to correct the
--   arguments in question. See the documentation of
--   @fixExpressionArgsOfTypeAliases@ for some more context.
exprArg :: SourcePos -> String -> BareTypeParsed -> ExprV LocSymbol
exprArg l msg = notracepp ("exprArg: " ++ msg) . go
  where
    go :: BareTypeParsed -> ExprV LocSymbol
    go (RExprArg e)     = val e
    go (RVar (BTV x) _) = EVar x
    go (RApp x [] [] _) = EVar (getLHNameSymbol <$> btc_tc x)
    go (RApp f ts [] _) = eApps (EVar (renameAmbiguousCtor . getLHNameSymbol <$> btc_tc f)) (go <$> ts)
    go (RAppTy t1 t2 _) = EApp (go t1) (go t2)
    go z                = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (show $ parsedToBareType z) msg
    sp                  = Just (LH.sourcePosSrcSpan l)

renameAmbiguousCtor :: Symbol -> Symbol
renameAmbiguousCtor x
  | Just n <- isTyTupleSizedSymbol x = tmTupleSizedSymbol n
  | otherwise = x

-- | A type alias 'lookupInScopeEnv' that distinguishes locally defined names
-- from imported ones based on their resolution status:
-- unresolved names correspond to type aliases defined in the current module,
-- whereas all imported names are expected to be resolved.
resolveTypeAlias
   :: InScopeEnv (RTAlias Symbol a)
   -> Symbol
   -> TypeAliasResolution (RTAlias Symbol a)
resolveTypeAlias taliases s = case lookupInScopeEnv taliases  s of
  Right ns -> let (imported, local) =
                    partition (\(_,lhname,_) -> isResolvedLogicName lhname ) ns
              in FoundTypeAliases imported local
  Left alts -> NoSuchTypeAlias alts

-- | When resolving type aliases we either find matching 'LHName's
-- or similar, but distinct, 'Symbol's.
data TypeAliasResolution a
  = NoSuchTypeAlias [Symbol]
  | FoundTypeAliases
      { tarImported :: [(GHC.Module, LHName, a)]
      , tarLocallyDefined :: [(GHC.Module, LHName, a)]
      }

errResolveTypeAlias :: LocSymbol -> TypeAliasResolution (RTAlias x a) -> Error
errResolveTypeAlias ls (FoundTypeAliases imported local) =
  ErrDupNames (LH.fSrcSpan ls) "type alias" (pprint $ val ls)
    (
      -- Currently, multiple local definitions prevent this error from being raised,
      -- because duplicate names are discarded when constructing the alias environment
      -- for each individual module,
      -- and a local alias always shadows any imported one. Such duplicates are detected
      -- later during validation of the final target spec.
      --
      -- Also, note that collected local type alias names remain unresolved at this stage,
      -- so we must extract their symbol using a function that can safely handle unresolved
      -- names.
      map (\(_, lhn, rta) -> pprint (getLHNameSymbol lhn)
                             PJ.<+>
                             PJ.text "defined in current module at"
                             PJ.<+>
                             pprint  (LH.fSrcSpan . rtName $ rta)
          )
          local
     ++
     map (\(m, lhn, rta) -> pprint (lhNameToUnqualifiedSymbol lhn)
                            PJ.<+>
                            PJ.text "imported from module"
                            PJ.<+>
                            PJ.text (GHC.moduleNameString (GHC.moduleName m))
                            PJ.<+>
                            PJ.text "defined at"
                            PJ.<+>
                            pprint (LH.fSrcSpan . rtName $ rta)
         )
         imported
    )
errResolveTypeAlias ls (NoSuchTypeAlias alts) =
  errResolve alts "type alias" "Cannot resolve name" ls


-- | An environment of names in scope
--
-- We construct it using 'mkAliasEnv' and 'unionAliasEnvs' in such a way that each
-- symbol in the environment corresponds to all matching 'LHNames' along with
-- the aliases of the module we import it from.
-- Currently, the parameter is used to include the type alias representation when
-- we 'collectTypeAliases'.
type InScopeEnv a = SEnv [(GHC.ModuleName, (GHC.Module, LHName, a))]

type InScopeNonReflectedEnv = InScopeEnv ()

-- | Looks for the 'LHName's in scope with the given symbol,
-- taking possible qualification prefixes into account.
-- Returns a list of close but different symbols or a non-empty list
-- with the matched names.
lookupInScopeEnv
  :: InScopeEnv a -> Symbol -> Either [Symbol] [(GHC.Module, LHName, a)]
lookupInScopeEnv env s = do
    -- The symbol might be qualified or not,
    -- but we use the unqualified symbol for the lookup.
    let n = LH.dropModuleNames s
    case lookupSEnvWithDistance n env of
      Alts closeSyms -> Left closeSyms
      F.Found xs -> do
         let q = LH.takeModuleNames s
         case filter ((GHC.mkFastString (symbolString q) ==) . GHC.moduleNameFS . fst) xs of
           [] -> Left $ map (maybeQualifySymbol n . symbol . GHC.moduleNameString . fst) xs
           ys -> Right $ map snd ys
  where
    maybeQualifySymbol n m =
      if m == "" then n else LH.qualifySymbol m n

-- | Builds an environment of non-reflected names in scope from the module
-- imports for the current module, the spec of the current module, and the specs
-- of the dependencies.
--
-- Also returns a LogicNameEnv constructed from the same names.
-- Also returns the names of reflected private functions.
-- Also returns the set of all names that aren't handled yet by name resolution.
makeLogicEnvs
  :: GHC.ImportedMods
  -> GHC.Module
  -> BareSpecParsed
  -> TargetDependencies
  -> ( InScopeNonReflectedEnv
     , LogicNameEnv
     , HS.HashSet LocSymbol
     )
makeLogicEnvs impMods thisModule spec dependencies =
    let depsLogicNames =
          map (fmap collectLiftedSpecLogicNames) dependencyPairs
        logicNames =
          (thisModule, thisModuleNames) : depsLogicNames
        nonReflectedNamesWithUnit =
          map
            (second $ map (, ()) . filter isNonReflectedLogicName)
            logicNames
        thisModuleNames = concat
          [ [ reflectLHName thisModule (val n)
            | n <- concat
              [ map fst (asmReflectSigs spec)
              , HS.toList (reflects spec)
              , HS.toList (opaqueReflects spec)
              , HS.toList (inlines spec)
              , HS.toList (hmeas spec)
              ]
            ]
          , [ val (msName m) | m <- measures spec ]
          , [ val (msName m) | m <- cmeasures spec ]
          , map fst $
             concatMap DataDecl.dcFields $ concat $
             mapMaybe DataDecl.tycDCons $
             dataDecls spec
          , [ val (rtName ea) | ea <- ealiases spec ]
          ]
        privateReflectNames =
          mconcat $
            privateReflects spec : map (liftedPrivateReflects . snd) dependencyPairs
     in
        ( unionAliasEnvs $ map (mkAliasEnv thisModule impMods) nonReflectedNamesWithUnit
        , mkLogicNameEnv (concatMap snd logicNames)
        , privateReflectNames
        )
  where
    dependencyPairs = map (first GHC.unStableModule) $ HM.toList $ getDependencies dependencies

    mkLogicNameEnv names =
      LogicNameEnv
        { lneLHName = fromListSEnv [ (lhNameToResolvedSymbol n, n) | n <- names ]
        , lneReflected = GHC.mkNameEnv [(rn, n) | n <- names, Just rn <- [maybeReflectedLHName n]]
        }

unionAliasEnvs :: forall a. [InScopeEnv a] -> InScopeEnv a
unionAliasEnvs =
    coerce .
    -- We make sure that the module alias and the 'LHName' effectively disambiguate
    -- the occurrence of a symbol. This is because the same name can come from
    -- several imported modules.
    HM.map (nubBy (\(alias1, (_, n1, _)) (alias2, (_, n2, _)) -> alias1 == alias2 && n1 == n2)) .
    foldl' (HM.unionWith (++)) HM.empty .
    coerce @_ @[HM.HashMap Symbol [(GHC.ModuleName, (GHC.Module, LHName, a))]]

-- | Builds a symbol lookup environment from a list of names associated with the
-- module they were extracted from, adding any import aliases that module may
-- have within the current module (if it was imported directly).
mkAliasEnv:: GHC.Module -> GHC.ImportedMods -> (GHC.Module, [(LHName, a)]) -> InScopeEnv a
mkAliasEnv thisModule impMods (m, lhnames) =
    let aliases = moduleAliases thisModule impMods m
     in fromListSEnv
          -- Note that when building a name environment for the current module
          -- we might process unresolved names here.
          [ (LH.dropModuleNames $ getLHNameSymbol lhname
            , map (,(m, lhname, x)) aliases)
          | (lhname, x) <- lhnames
          ]

-- | Produces the list of aliases a module is imported with.
-- The first parameter holds the reference to the current module.
-- Transitive dependencies get an empty alias list.
moduleAliases :: GHC.Module -> GHC.ImportedMods -> GHC.Module -> [GHC.ModuleName]
moduleAliases thisModule impMods m =
    case Map.lookup m impMods of
      -- Aliases for imported modules.
      Just impBys -> concatMap imvAliases $ GHC.importedByUser impBys
      Nothing
        | thisModule == m ->
          -- Aliases for the current module.
          [GHC.moduleName m, GHC.mkModuleName ""]
        | otherwise ->
          -- For LHAssumptions modules, use the aliases of the unsuffixed module.
          concatMap imvAliases $ GHC.importedByUser $
            concat $ maybeToList $ do
              pString <- dropLHAssumptionsSuffix
              pMod <- findDependency pString
              Map.lookup pMod impMods
  where
    dropLHAssumptionsSuffix =
      let mString = GHC.moduleNameString (GHC.moduleName m)
          sfx = "_LHAssumptions"
       in if isSuffixOf sfx mString then
            Just $ dropEnd (length sfx) mString
          else
            Nothing

    findDependency ms =
      find ((ms ==) . GHC.moduleNameString . GHC.moduleName) $
      Map.keys impMods

    imvAliases imv
      | GHC.imv_qualified imv = [GHC.imv_name imv]
      | otherwise = [GHC.imv_name imv, GHC.mkModuleName ""]

collectLiftedSpecLogicNames :: LiftedSpec -> [LHName]
collectLiftedSpecLogicNames sp = concat
    [ map fst (HS.toList $ liftedExpSigs sp)
    , map (val . msName) (HM.elems $ liftedMeasures sp)
    , map (val . msName) (HM.elems $ liftedCmeasures sp)
    , map (val . msName) (HS.toList $ liftedOmeasures sp)
    , map fst $ concatMap DataDecl.dcFields $ concat $
        mapMaybe DataDecl.tycDCons $
        HS.toList $ liftedDataDecls sp
    , map  (val . rtName) $ HS.toList $ liftedEaliases sp
    ]

-- | Resolves names in the logic namespace
--
-- Returns the renamed spec.
-- Adds in the monadic state the errors about ambiguous or missing names, and
-- the names of data constructors that are found during renaming.
resolveLogicNames
  :: Config
  -> GHC.Module
  -> InScopeNonReflectedEnv
  -> GHC.GlobalRdrEnv
  -> LogicMap
  -> LocalVars
  -> LogicNameEnv
  -> HS.HashSet LocSymbol
  -> HS.HashSet Symbol
  -> BareSpecParsed
  -> State RenameOutput BareSpecLHName
resolveLogicNames cfg thisModule env globalRdrEnv lmap0 localVars lnameEnv privateReflectNames depsInlinesAndDefines sp = do
    -- Instance measures must be defined for names of class measures.
    -- The names of class measures should be in @env@
    imeasures <- mapM (mapMeasureNamesM resolveIMeasLogicName) (imeasures sp)
    emapSpecM
      (bscope cfg)
      (map localVarToSymbol . maybe [] lvdLclEnv . (GHC.lookupNameEnv (lvNames localVars) <=< getLHGHCName))
      resolveLogicName
      (emapBareTypeVM (bscope cfg) resolveLogicName)
      sp {imeasures}
  where
    resolveIMeasLogicName lx =
      case val lx of
        LHNUnresolved LHLogicName s -> (<$ lx) <$> resolveLogicName [] (s <$ lx)
        _ -> panic (Just $ LH.fSrcSpan lx) $ "unexpected name: " ++ show lx

    localVarToSymbol = F.symbol . GHC.occNameString . GHC.nameOccName . GHC.varName

    resolveLogicName :: [Symbol] -> LocSymbol -> State RenameOutput LHName
    resolveLogicName ss ls
        -- The name is local
      | elem s ss = return $ makeLocalLHName s
      | otherwise =
        case lookupInScopeEnv env s of
          Left alts ->
            -- If names are not in the environment, they must be data constructors,
            -- or they must be reflected functions, or they must be in the logicmap.
            case resolveDataConName ls `mplus` resolveVarName lmap0 ls of
              Just m -> m
              Nothing
                | elem s wiredInNames ->
                  return $ makeLocalLHName s
                | otherwise -> do
                    addError $ errResolve alts "logic name" "Cannot resolve name" ls
                    return $ makeLocalLHName s
          Right [(_, lhname, _)] -> pure lhname
          -- In case of multiple matches, we give precedence to locally defined
          -- logic entities for the user to be able to overwrite them.
          -- TODO: When a mechanism allowing to specify explicitly which logic names
          -- are imported is in place, we should cosider notifying the ambiguity directly.
          Right names ->
            case filter ((== thisModule) . logicNameOriginModule . Misc.snd3) names of
              [(_, lhname, _)] -> pure lhname
              _ -> do addError $ errDupInScopeNames ls names
                      return $ makeLocalLHName s
      where
        s = val ls
        wiredInNames =
           map fst wiredSortedSyms ++
           map (lhNameToResolvedSymbol . fst) (concatMap (DataDecl.dcpTyArgs . val) wiredDataCons)
        errDupInScopeNames locSym inScopeNames =
          ErrDupNames
            (LH.fSrcSpan locSym)
            "non-reflected logic entity"
            (pprint (val locSym))
            [ pprint (lhNameToResolvedSymbol n) PJ.<+>
              PJ.text
                ("imported from " ++ GHC.moduleNameString (GHC.moduleName m))
            | (m, n, _) <- inScopeNames
            ]

    resolveDataConName ls
      | unqualifiedS == ":" = Just $
        return $ makeLogicLHName unqualifiedS (GHC.nameModule consDataConName) (Just consDataConName)
      | unqualifiedS == "[]" = Just $
        return $ makeLogicLHName unqualifiedS (GHC.nameModule nilDataConName) (Just nilDataConName)
      | Just arity <- isTupleDC (symbolText s) = Just $
          let dcName = tupleDataConName arity
           in return $ makeLogicLHName s (GHC.nameModule dcName) (Just dcName)
      where
        unqualifiedS = LH.dropModuleNames s
        nilDataConName = GHC.getName $ GHC.dataConWorkId GHC.nilDataCon
        consDataConName = GHC.getName $ GHC.dataConWorkId GHC.consDataCon
        tupleDataConName = GHC.getName . GHC.dataConWorkId . GHC.tupleDataCon GHC.Boxed
        s = val ls
        isTupleDC t
          | Text.isPrefixOf "(" t && Text.isSuffixOf ")" t &&
            Text.all (== ',') (Text.init $ Text.tail t)
          = Just $ Text.length t - 2
          | otherwise
          = Nothing
    resolveDataConName s =
      case GHC.lookupGRE globalRdrEnv (mkLookupGRE (LHDataConName LHAnyModuleNameF) $ val s) of
        [e] -> do
          let n = GHC.greName e
          Just $ do
            let lhName = makeLogicLHName (symbol $ GHC.getOccString n) (GHC.nameModule n) (Just n)
            addName lhName
            addDataConsName lhName
            return lhName
        [] ->
          Nothing
        es ->
          Just $ do
            addError
              (ErrDupNames
                 (LH.fSrcSpan s)
                 "data constructor"
                 (pprint $ val s)
                 (map (PJ.text . GHC.showPprUnsafe) es)
              )
            return $ makeLocalLHName $ val s

    -- Resolves names of reflected functions or names in the logic map
    --
    -- Names of reflected functions are resolved here because, to be in scope,
    -- we ask the corresponding Haskell name to be in scope. In contrast, the
    -- @InScopeNonReflectedEnv@ indicates where the reflect annotations were
    -- imported from, but not where the Haskell names were imported from.
    resolveVarName lmap s = do
      let gres =
            GHC.lookupGRE globalRdrEnv $
            mkLookupGRE (LHVarName LHAnyModuleNameF) (val s)
          refls = mapMaybe (findReflection . GHC.greName) gres
      case refls of
        [lhName] -> Just $ return lhName
        _ | HS.member s privateReflectNames
          -> Just $ return $ makeLocalLHName (val s)
          | otherwise
          -> case gres of
          [e] -> do
            let n = GHC.greName e
            -- See [NOTE:EXPRESSION-ALIASES]
            if HM.member (symbol n) (lmSymDefs lmap) || HS.member (symbol n) depsInlinesAndDefines then
              Just $ do
                let lhName = makeLogicLHName (symbol $ GHC.getOccString n) (GHC.nameModule n) Nothing
                addName lhName
                return lhName
            else
              Nothing
          [] ->
            Nothing
          es ->
            Just $ do
              addError
                 (ErrDupNames
                   (LH.fSrcSpan s)
                   "variable"
                   (pprint $ val s)
                   (map (PJ.text . GHC.showPprUnsafe) es)
                 )
              return $ makeLocalLHName $ val s

    findReflection :: GHC.Name -> Maybe LHName
    findReflection n = GHC.lookupNameEnv (lneReflected lnameEnv) n

mapMeasureNamesM :: Monad m => (Located LHName -> m (Located LHName)) -> MeasureV v ty ctor -> m (MeasureV v ty ctor)
mapMeasureNamesM f m = do
    msName <- f (msName m)
    msEqns <- mapM mapDefNameM (msEqns m)
    return m {msName, msEqns}
  where
    mapDefNameM d = do
      measure <- f (measure d)
      return d {measure}

mapDataDeclFieldNamesM :: Monad m => (LHName -> m LHName) -> DataDecl.DataDeclP v ty -> m (DataDecl.DataDeclP v ty)
mapDataDeclFieldNamesM f d = do
    tycDCons <- traverse (mapM (mapDataCtorFieldsM f)) (DataDecl.tycDCons d)
    return d{DataDecl.tycDCons}
  where
    mapDataCtorFieldsM :: Monad m => (LHName -> m LHName) -> DataDecl.DataCtorP ty -> m (DataDecl.DataCtorP ty)
    mapDataCtorFieldsM f1 c = do
      dcFields <- mapM (\(n, t) -> (, t) <$> f1 n) (DataDecl.dcFields c)
      return c{DataDecl.dcFields}

toBareSpecLHName :: Config -> LogicNameEnv -> BareSpec -> BareSpecLHName
toBareSpecLHName cfg lenv sp0 = runIdentity $ go sp0
  where
    -- This is implemented with a monadic traversal to reuse the logic
    -- that collects the local symbols in scope.
    go :: BareSpec -> Identity BareSpecLHName
    go sp =
      emapSpecM
        (bscope cfg)
        (const [])
        symToLHName
        (emapBareTypeVM (bscope cfg) symToLHName)
        sp

    symToLHName = symbolToLHName "toBareSpecLHName" lenv unhandledNames

    unhandledNames = HS.fromList $ map fst $ expSigs sp0

-- | Uses the logic name environment to convert a resolved 'Symbol' to 'LHName'.
-- Symbols not present in the environment correspond to local symbols (e.g.
-- bounded variables) or are explicitly left unhandled.
symbolToLHName :: String -> LogicNameEnv -> HS.HashSet Symbol -> [Symbol] -> Symbol -> Identity LHName
symbolToLHName caller lenv unhandledNames ss s
  | elem s ss = return $ makeLocalLHName s
  | otherwise =
    case lookupSEnv s (lneLHName lenv) of
      Nothing -> do
        unless (HS.member s unhandledNames) $
          panic Nothing $ caller ++ ": cannot find " ++ show s
        return $ makeLocalLHName s
      Just lhname -> return lhname
